Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
ACTIVE(diff(X, Y)) → P(X)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → LEQ(active(X1), X2)
PROPER(leq(X1, X2)) → PROPER(X1)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(diff(X, Y)) → IF(leq(X, Y), 0, s(diff(p(X), Y)))
ACTIVE(p(X)) → P(active(X))
PROPER(s(X)) → S(proper(X))
P(ok(X)) → P(X)
ACTIVE(diff(X, Y)) → S(diff(p(X), Y))
ACTIVE(diff(X1, X2)) → DIFF(active(X1), X2)
ACTIVE(s(X)) → ACTIVE(X)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
PROPER(leq(X1, X2)) → LEQ(proper(X1), proper(X2))
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
ACTIVE(leq(X1, X2)) → LEQ(X1, active(X2))
PROPER(p(X)) → PROPER(X)
TOP(mark(X)) → PROPER(X)
P(mark(X)) → P(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → LEQ(X, Y)
PROPER(leq(X1, X2)) → PROPER(X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
DIFF(mark(X1), X2) → DIFF(X1, X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → DIFF(p(X), Y)
PROPER(diff(X1, X2)) → DIFF(proper(X1), proper(X2))
TOP(ok(X)) → TOP(active(X))
S(mark(X)) → S(X)
PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X2)
ACTIVE(leq(s(X), s(Y))) → LEQ(X, Y)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
DIFF(X1, mark(X2)) → DIFF(X1, X2)
PROPER(p(X)) → P(proper(X))
ACTIVE(diff(X1, X2)) → DIFF(X1, active(X2))
PROPER(diff(X1, X2)) → PROPER(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
ACTIVE(diff(X, Y)) → P(X)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
ACTIVE(leq(X1, X2)) → LEQ(active(X1), X2)
PROPER(leq(X1, X2)) → PROPER(X1)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(diff(X, Y)) → IF(leq(X, Y), 0, s(diff(p(X), Y)))
ACTIVE(p(X)) → P(active(X))
PROPER(s(X)) → S(proper(X))
P(ok(X)) → P(X)
ACTIVE(diff(X, Y)) → S(diff(p(X), Y))
ACTIVE(diff(X1, X2)) → DIFF(active(X1), X2)
ACTIVE(s(X)) → ACTIVE(X)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
PROPER(leq(X1, X2)) → LEQ(proper(X1), proper(X2))
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
ACTIVE(leq(X1, X2)) → LEQ(X1, active(X2))
PROPER(p(X)) → PROPER(X)
TOP(mark(X)) → PROPER(X)
P(mark(X)) → P(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → LEQ(X, Y)
PROPER(leq(X1, X2)) → PROPER(X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
DIFF(mark(X1), X2) → DIFF(X1, X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(diff(X, Y)) → DIFF(p(X), Y)
PROPER(diff(X1, X2)) → DIFF(proper(X1), proper(X2))
TOP(ok(X)) → TOP(active(X))
S(mark(X)) → S(X)
PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X2)
ACTIVE(leq(s(X), s(Y))) → LEQ(X, Y)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
DIFF(X1, mark(X2)) → DIFF(X1, X2)
PROPER(p(X)) → P(proper(X))
ACTIVE(diff(X1, X2)) → DIFF(X1, active(X2))
PROPER(diff(X1, X2)) → PROPER(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 8 SCCs with 20 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DIFF(X1, mark(X2)) → DIFF(X1, X2)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
DIFF(mark(X1), X2) → DIFF(X1, X2)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DIFF(X1, mark(X2)) → DIFF(X1, X2)
DIFF(ok(X1), ok(X2)) → DIFF(X1, X2)
DIFF(mark(X1), X2) → DIFF(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ(ok(X1), ok(X2)) → LEQ(X1, X2)
LEQ(X1, mark(X2)) → LEQ(X1, X2)
LEQ(mark(X1), X2) → LEQ(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(p(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(diff(X1, X2)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X1)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(diff(X1, X2)) → PROPER(X2)
PROPER(p(X)) → PROPER(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(diff(X1, X2)) → PROPER(X1)
PROPER(leq(X1, X2)) → PROPER(X2)
PROPER(leq(X1, X2)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesProof
QDP
                ↳ QDPSizeChangeProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(diff(X1, X2)) → ACTIVE(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X1)
ACTIVE(leq(X1, X2)) → ACTIVE(X2)
ACTIVE(diff(X1, X2)) → ACTIVE(X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
QDP
            ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
p(mark(X)) → mark(p(X))
s(mark(X)) → mark(s(X))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
p(ok(X)) → ok(p(X))
s(ok(X)) → ok(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0   
POL(TOP(x1)) = 2·x1   
POL(active(x1)) = 2·x1   
POL(diff(x1, x2)) = 2·x1 + x2   
POL(false) = 0   
POL(if(x1, x2, x3)) = x1 + 2·x2 + x3   
POL(leq(x1, x2)) = x1 + x2   
POL(mark(x1)) = x1   
POL(ok(x1)) = 2·x1   
POL(p(x1)) = x1   
POL(proper(x1)) = x1   
POL(s(x1)) = x1   
POL(true) = 0   



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
QDP
                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(mark(X)) → TOP(proper(X)) at position [0] we obtained the following new rules:

TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(false)) → TOP(ok(false))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
QDP
                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(ok(X)) → TOP(active(X)) at position [0] we obtained the following new rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(ok(leq(0, x0))) → TOP(mark(true))
TOP(ok(leq(s(x0), 0))) → TOP(mark(false))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(p(0))) → TOP(mark(0))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
QDP
                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(0, x0))) → TOP(mark(true))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), 0))) → TOP(mark(false))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(mark(true)) → TOP(ok(true))
TOP(ok(p(0))) → TOP(mark(0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ DependencyGraphProof
QDP
                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


TOP(ok(p(s(x0)))) → TOP(mark(x0))
The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = x1   
POL(diff(x1, x2)) = 0   
POL(false) = 0   
POL(if(x1, x2, x3)) = x2 + x3   
POL(leq(x1, x2)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(p(x1)) = 1 + x1   
POL(proper(x1)) = x1   
POL(s(x1)) = x1   
POL(true) = 0   

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
active(diff(X1, X2)) → diff(active(X1), X2)
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
diff(mark(X1), X2) → mark(diff(X1, X2))
active(diff(X1, X2)) → diff(X1, active(X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(p(0)) → mark(0)
active(p(s(X))) → mark(X)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
QDP
                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


TOP(ok(diff(x0, x1))) → TOP(mark(if(leq(x0, x1), 0, s(diff(p(x0), x1)))))
The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = 0   
POL(diff(x1, x2)) = 1   
POL(false) = 0   
POL(if(x1, x2, x3)) = x2 + x3   
POL(leq(x1, x2)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(p(x1)) = 0   
POL(proper(x1)) = x1   
POL(s(x1)) = 0   
POL(true) = 0   

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof
QDP
                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
The remaining pairs can at least be oriented weakly.

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
Used ordering: Polynomial interpretation with max and min functions [25]:

POL(0) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = 0   
POL(diff(x1, x2)) = 0   
POL(false) = 0   
POL(if(x1, x2, x3)) = 1 + x2 + x3   
POL(leq(x1, x2)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(p(x1)) = 0   
POL(proper(x1)) = x1   
POL(s(x1)) = 0   
POL(true) = 0   

The following usable rules [17] were oriented:

p(mark(X)) → mark(p(X))
s(ok(X)) → ok(s(X))
proper(p(X)) → p(proper(X))
p(ok(X)) → ok(p(X))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(mark(X1), X2) → mark(leq(X1, X2))
s(mark(X)) → mark(s(X))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
diff(mark(X1), X2) → mark(diff(X1, X2))
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ UsableRulesReductionPairsProof
              ↳ QDP
                ↳ Narrowing
                  ↳ QDP
                    ↳ Narrowing
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
QDP

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(diff(x0, x1))) → TOP(diff(active(x0), x1))
TOP(ok(diff(x0, x1))) → TOP(diff(x0, active(x1)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(leq(x0, x1))) → TOP(leq(active(x0), x1))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(leq(x0, x1))) → TOP(leq(x0, active(x1)))
TOP(mark(diff(x0, x1))) → TOP(diff(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(leq(s(x0), s(x1)))) → TOP(mark(leq(x0, x1)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(leq(x0, x1))) → TOP(leq(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))

The TRS R consists of the following rules:

active(p(0)) → mark(0)
active(p(s(X))) → mark(X)
active(leq(0, Y)) → mark(true)
active(leq(s(X), 0)) → mark(false)
active(leq(s(X), s(Y))) → mark(leq(X, Y))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(diff(X, Y)) → mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
active(p(X)) → p(active(X))
active(s(X)) → s(active(X))
active(leq(X1, X2)) → leq(active(X1), X2)
active(leq(X1, X2)) → leq(X1, active(X2))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(diff(X1, X2)) → diff(active(X1), X2)
active(diff(X1, X2)) → diff(X1, active(X2))
diff(mark(X1), X2) → mark(diff(X1, X2))
diff(X1, mark(X2)) → mark(diff(X1, X2))
diff(ok(X1), ok(X2)) → ok(diff(X1, X2))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
leq(mark(X1), X2) → mark(leq(X1, X2))
leq(X1, mark(X2)) → mark(leq(X1, X2))
leq(ok(X1), ok(X2)) → ok(leq(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
proper(p(X)) → p(proper(X))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(leq(X1, X2)) → leq(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(diff(X1, X2)) → diff(proper(X1), proper(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.